using System;
using System.Collections;
using System.Diagnostics;

namespace Meta
{
	public class TypeDependency {
		public TypeDependency(TypeVariable dependent, string message) {
			this.dependent = dependent;
			this.message = message;
		}
		public readonly TypeVariable dependent;
		public readonly string message;
	}

	/// <summary>
	/// Summary description for TypeVariable.
	/// </summary>
	/// 
	public class TypeVariable : IPrettyPrintableType
	{
		// Instance fields
		// Basic information
		public Type currentType;										// Current type
		TypeVariable representative;						// Representative of this set's equivalence class
		readonly int uid;
		static int nextuid=0;
		public static bool TraceRefinement = false;
		bool locked = false;
		bool trace = false;

		public TypeVariable Representative {
			get {
				TypeVariable r = representative;
				if (r==null)
					return this;
				else {
					r = representative.Representative;
					representative = r;
					return r;
				}
			}
		}

		public Type Type {
			get {
				return Representative.currentType;
			}
		}

		public bool isWired=false;                           // True if this is from a declaration and can't be refined
		public Expression expression;                     // Expression of this this represents the type

		// Update propagation information
		ArrayList dependencies = new ArrayList();   // TypeVariables bounded by this variable
		ArrayList updateThunks = new ArrayList();   // Procedures to call when this variable is refined

		public static Procedure warnHook;

		public TypeVariable() : this(typeof(object), null) {}
		public TypeVariable(Type type, Expression e)
		{
			this.currentType = type;
			this.expression = e;
			uid = nextuid++;
		}

		public TypeVariable(Type type, Expression e, bool trace) : this(type, e) {
			this.trace = trace;
		}

		string IPrettyPrintableType.PrettyPrint(Hashtable h) {
			TypeVariable r = Representative;
			if (h.ContainsKey(r)) {
				int num = (int)h[r];
				if (num>=0) {
					h[r] = ~num;
					if (r.currentType==typeof(object))
						return string.Format("T{0}", num);
					else
						return string.Format("T{0}\u2264{1}", num, TypeWalker.Format(r.currentType, h));
				} else
					return string.Format("T{0}", ~num);
			} else
				return TypeWalker.Format(r.currentType, h);
		}

		public override string ToString() {
			if (Type==null)
				return "TypeVariable null";
			else if (representative==null)
				return String.Format("TypeVariable {0}:{1}", uid, Type.Name);
			else
				return String.Format("TypeVariable {0}={1}:{2}", uid, Representative.uid, Type.Name);
		}


		public void WireType(Type t) {
			//Debug.Assert(representative==null, "Wiring non-representative typevar");
			Debug.Assert(!locked, "wiring locked TypeVariable");
			if (representative==null) {
				if (TraceRefinement || trace)
					TopLevel.Log("Wire-type", this, t, "was", currentType);
				currentType = t;
				isWired = true;
			} else
				Representative.WireType(t);
		}


		// Assert bound; returns whether the TypeVariable's bound was tightened.
		// If bindingEnvironment is non-null, this does a unification, possibly instantiating the type structure.
		public virtual bool Bound(Type t, string message, Hashtable bindingEnvironment, Expression site) {
			bool instantiating = bindingEnvironment!=null;

			// Make sure we're doing something sensible.
//			if (locked)
//				throw new Exception("bounding locked TypeVariable");
			if (representative != null)
				return Representative.Bound(t, message, bindingEnvironment, site);

			// Log the operation
			if (TraceRefinement || trace)
				Meta.TopLevel.Log("bound", this.expression, this, t, "was", this.currentType);

			// Check for trivial cases
			if (currentType==typeof(void) || t==currentType || t==null)
				return false;

			if (instantiating && t is ITypeExpression) {
				//
				// This is the hard case.
				// We need to unify currentType with t, copying interior TypeVariables as necessary.
				//
				if (currentType!=null && currentType.IsArray)
					currentType = new ListOf(new TypeVariable(currentType.GetElementType(), expression));
				if (currentType==null || currentType.GetType()==t.GetType() || TypeLattice.SubTypeInclusive(t, currentType))
					// This is a weird ad-hoc version of sorted unification
					return Instantiate((ITypeExpression)t, message, bindingEnvironment, site);
				else if (t is ListOf && typeof(IList).IsAssignableFrom(currentType))
					// We can't propagate any type information here.
					return false;
				else {
					if (TraceRefinement || trace)
						TopLevel.Log("Trying to unify structually incompatible types", currentType, t);
					Warn(message, expression, "Can't unify types", site);
					return false;
				}
			} else {
				//
				// Easy case.
				// We don't need to do any binding or instantiation.
				//
				if (t is LUBType)
					// Just take the current type bound from t.
					t = ((LUBType)t).Type;

				// Nothing to do if t is a supertype of our current bound.
				if (currentType!=null && (currentType==t || TypeLattice.SubTypeInclusive(currentType, t)))
					return false;

				// Need to refine if it's a tighter bound
				if (currentType==null || TypeLattice.SubType(t, currentType)) {
					if (isWired)
						// It's an argument with a declared type; don't refine it.
						return false;

					// Tighten the bound
					Refine(t, bindingEnvironment, site);
					return true;
				} else
					// Failure: trying to apply a bound that isn't a subtype of the current bound.
					Warn(message, expression, null, site);
				return false;
			}
		}

		public virtual bool Bound(TypeVariable bound, string message, Hashtable bindingEnvironment, Expression site) {
			// Check if we're instantiating bound (i.e. copying and unifying)
			bool instantiating = bindingEnvironment!=null;

			if (bound==this)
				return false;

//			if (locked)
//				throw new Exception("bounding locked TypeVariable");
			if (TraceRefinement || trace)
				TopLevel.Log("Bound", this.expression, this, bound, message);

			// Resolve bindings on this and bound.
			bound = bound.Representative;
			if (representative!=null)
				return Representative.Bound(bound, message, bindingEnvironment, site);
			// If we're instantiating, check whether it's already in the binding environment and if so, equate.
			else if (instantiating && bindingEnvironment.ContainsKey(bound)) {
				if (TraceRefinement || trace)
					TopLevel.Log("Bound:", bound, "already in environment as", bindingEnvironment[bound], "equating to ", this);
				Equate(this, (TypeVariable)bindingEnvironment[bound], bindingEnvironment, site);
				return true;
			} else {
				// Tell bound to update us if it's refined
				bound.dependencies.Add(new TypeDependency(this, message));
				// Remember we're the local copy of bound if instantiating
				if (instantiating) {
					if (TraceRefinement || trace)
						TopLevel.Log("Bound: Store-environment", bound, this);
					bindingEnvironment[bound] = this;
				}
				// Okay, now do the real bounding.
				return Bound(bound.currentType, message, bindingEnvironment, site);
			}
		}

		// Assert these type variables are equal
		public static void Equate(TypeVariable t1, TypeVariable t2, Hashtable bindingEnvironment, Expression site) {
			// Canonicalize type variables
			TypeVariable r1 = t1.Representative;
			TypeVariable r2 = t2.Representative;

			// If already equated, then nothing to do.
			if (r1==r2) {
				if (TraceRefinement || t1.trace || t2.trace)
					Meta.TopLevel.Log("Equate: already =", t1.expression, t1, t2, t2.expression);
				return;
			}

			// We can't equate them if r2 is wired because we'll be rewritting its representative.
			if (r2.isWired || r2.locked) {
				// Swap them
				TypeVariable temp = r1;
				r1 = r2;
				r2 = temp;
			}
			//if (r1.isWired || r2.isWired)
			if (r2.isWired)
				throw new Exception("equating wired TypeVariable");
			if (r2.locked)
				throw new Exception("equating locked TypeVariable");


			if (TraceRefinement || t1.trace || t2.trace)
				Meta.TopLevel.Log("equate", t1.expression, t1, t2, t2.expression);

			Type bound = r2.currentType;
			//if (bound!=null && bound is LUBType)
			//	bound = ((LUBType)bound).Type;

			if (r1.currentType==null) {
				r1.currentType = bound;
				r1.PropagateDependencies(bound, bindingEnvironment, site);
			} else if (bound!=null) {
				if (TypeLattice.SubType(bound, r1.currentType)) {
					r1.currentType=bound;
					r1.PropagateDependencies(bound, bindingEnvironment, site);
				} else if (r1.currentType!=bound && !TypeLattice.SubType(r1.currentType, bound))
					Warn("Type conflict", site, "Equating incompatible types", site);
			}
			r2.representative = r1;
			r1.dependencies.AddRange(r2.dependencies);
			r1.updateThunks.AddRange(r2.updateThunks);
		}

		//
		// Called when t is a tighter bound than currentType
		// and we're not instantiating and/or t isn't a type expression
		//
		protected void Refine(Type t, Hashtable bindingEnvironment, Expression site) {
			if (TraceRefinement || trace)
				Meta.TopLevel.Log("refine", this, t, "was", currentType);
			if (t is ITypeExpression)
				// It's a type expression but we aren't instantiating; apply bound recursively.
				((ITypeExpression)t).SimpleBound(this, "Type conflict", site);
			else {
				if (locked)
					throw new Exception("Refining locked type variable");
				// It's an atomic type; just change the pointer
				currentType = t;
			}
			PropagateDependencies(t, bindingEnvironment, site);
		}

		void PropagateDependencies(Type t, Hashtable bindingEnvironment, Expression site) {
			// Propagate dependencies
			foreach (TypeDependency dependency in dependencies)
				dependency.dependent.Bound(t, dependency.message, bindingEnvironment, site);
			EvalStack e = EvalStack.CurrentThreadEvalStack;
			// Can't use foreach here because one thunk can potentially add other thunks.
			int thunkno=0;
			while (thunkno<updateThunks.Count) {
				Procedure p = (Procedure)updateThunks[thunkno];
				Procedure.TracedCall(p, e);
				thunkno++;
			}
		}

		//
		// Called when instantiating a type expression
		// Makes currentType be a fresh copy of t, bounded by t..
		//
		public bool Instantiate(ITypeExpression t, string message, Hashtable bindingEnvironment, Expression site) {
			if (TraceRefinement || trace)
				Meta.TopLevel.Log("bind", this, t);
			if (bindingEnvironment==null)
				bindingEnvironment = new Hashtable();

			//Console.Out.WriteLine("Instantiate {2}: {0}, {1}", this, t, this.expression);
			return t.Instantiate(this, message, bindingEnvironment, site);
		}

		public static bool Instantiate(TypeVariable t1, TypeVariable t2, string message, Hashtable bindingEnvironment, Expression site) {
//			if (t1.locked)
//				throw new Exception("binding locked TypeVariable");

			if (TraceRefinement || t1.trace || t2.trace)
				Meta.TopLevel.Log("bindvars", t1, t2);
			TypeVariable r2 = t2.Representative;
			if (bindingEnvironment!=null && bindingEnvironment.ContainsKey(r2) && bindingEnvironment[r2]!=t1) {
				// This is a duplicated variable, so we need to unify it.
				if (TraceRefinement || t1.trace || t2.trace)
					Meta.TopLevel.Log("bindvars: already in environment; equating");
				Equate(t1, (TypeVariable)bindingEnvironment[r2], bindingEnvironment, site);
				return true;
			} else {
				if (bindingEnvironment != null) {
					if (TraceRefinement || t1.trace || t2.trace)
						TopLevel.Log("Instantiate: Store-environment", r2, t1);
					bindingEnvironment[r2]=t1;
				}
				if (TraceRefinement || t1.trace || t2.trace)
					TopLevel.Log("bindvars: bounding ...");
				return t1.Bound(r2, message, bindingEnvironment, site);
			}
		}

		// Call thunk whenever this variable is refined.
		// We don't use events for this since we want them to be Meta Procedure objects rather than delegates
		public void AddRefinementHandler(Meta.Procedure thunk) {
			if (representative!=null)
				Representative.AddRefinementHandler(thunk);
			else
				updateThunks.Add(thunk);
		}

		public static void Warn(string message, Expression e, string detail, Expression site) {
			if (TraceRefinement)
				TopLevel.Log("Warn", message, e);
			Procedure.TracedCall(warnHook, message, e, detail, site);
		}
	}
}
